ody>

(*  Title:   StandardBorel.thy
    Author:  Michikazu Hirata, Tokyo Institute of Technology
*)

section  ‹Standard Borel Spaces›
theory StandardBorel
  imports "HOL-Probability.Probability"
begin

text ‹A standard Borel space is the Borel space associated with a Polish space.
      Here, we define standard Borel spaces in another, but equivallent, way.
      See @{cite "Heunen_2017"} Proposition 5. ›
abbreviation "real_borel ≡ borel :: real measure"
abbreviation "nat_borel ≡ borel :: nat measure"
abbreviation "ennreal_borel ≡ borel :: ennreal measure"
abbreviation "bool_borel ≡ borel :: bool measure"


subsection ‹ Definition ›
locale standard_borel =
  fixes M :: "'a measure"
  assumes exist_fg: "∃f ∈ M →⇩M real_borel. ∃g ∈ real_borel →⇩M M.
                     ∀x ∈ space M.  (g ∘ f) x = x"
begin

abbreviation "fg ≡ (SOME k. (fst k) ∈ M →⇩M real_borel ∧ 
                           (snd k) ∈ real_borel →⇩M M ∧
                           (∀x ∈ space M.  ((snd k) ∘ (fst k)) x = x))"

definition "f ≡ (fst fg)"
definition "g ≡ (snd fg)"

lemma 
  shows f_meas[simp,measurable]    :  "f ∈ M →⇩M real_borel"
    and g_meas[simp,measurable]    :  "g ∈ real_borel →⇩M M"
    and gf_comp_id[simp]:  "⋀x. x ∈ space M ⟹ (g ∘ f) x = x"
                           "⋀x. x ∈ space M ⟹ g (f x) = x"
proof -
  obtain f' g' where h:
    "f' ∈ M →⇩M real_borel" "g' ∈ real_borel →⇩M M" "∀x ∈ space M.  (g' ∘ f') x = x"
    using exist_fg by blast
  have "f ∈ borel_measurable M ∧ g ∈ real_borel →⇩M M ∧ (∀x∈space M. (g ∘ f) x = x)"
    unfolding f_def g_def
    by(rule someI2[where a="(f',g')"]) (use h in auto)
  thus "f ∈ borel_measurable M" "g ∈ real_borel →⇩M M"
       "⋀x. x ∈ space M ⟹ (g ∘ f) x = x" "⋀x. x ∈ space M ⟹ g (f x) = x"
    by auto
qed

lemma standard_borel_sets[simp]:
  assumes "sets M = sets Y"
  shows "standard_borel Y"
  unfolding standard_borel_def
  using measurable_cong_sets[OF assms refl,of real_borel] measurable_cong_sets[OF refl assms,of real_borel] sets_eq_imp_space_eq[OF assms] exist_fg
  by simp

lemma f_inj:
  "inj_on f (space M)"
  by standard (use gf_comp_id(2) in fastforce)

lemma singleton_sets:
  assumes "x ∈ space M"
    shows "{x} ∈ sets M"
proof -
  let ?y = "f x"
  let ?U = "f -` {?y}"
  have "?U ∩ space M ∈ sets M"
    using borel_measurable_vimage f_meas by blast
  moreover have "?U ∩ space M = {x}"
    using assms f_inj by(auto simp:inj_on_def)
  ultimately show ?thesis
    by simp
qed

lemma countable_space_discrete:
  assumes "countable (space M)"
  shows "sets M = sets (count_space (space M))"
proof
  show "sets (count_space (space M)) ⊆ sets M"
  proof auto
    fix U
    assume 1:"U ⊆ space M"
    then have 2:"countable U"
      using assms countable_subset by auto
    have 3:"U = (⋃x∈U. {x})" by auto
    moreover have "... ∈ sets M"
      by(rule sets.countable_UN''[of U "λx. {x}"]) (use 1 2 singleton_sets in auto)
    ultimately show "U ∈ sets M"
      by simp
  qed
qed (simp add: sets.sets_into_space subsetI)

end

lemma standard_borelI:
  assumes "f ∈ Y →⇩M real_borel"
          "g ∈ real_borel →⇩M Y"
      and "⋀y. y ∈ space Y ⟹  (g ∘ f) y = y"
    shows "standard_borel Y"
  unfolding standard_borel_def
  by (intro bexI[OF _ assms(1)] bexI[OF _ assms(2)]) (auto dest: assms(3))


locale standard_borel_space_UNIV = standard_borel +
  assumes space_UNIV:"space M = UNIV"
begin

lemma gf_comp_id'[simp]:
  "g ∘ f = id" "g (f x) = x"
  using space_UNIV gf_comp_id
  by(simp_all add: id_def comp_def)

lemma f_inj':
  "inj f"
  using f_inj by(simp add: space_UNIV)

lemma g_surj':
  "surj g"
  using gf_comp_id'(2) surjI by blast

end

lemma standard_borel_space_UNIVI:
  assumes "f ∈ Y →⇩M real_borel"
          "g ∈ real_borel →⇩M Y"
          "(g ∘ f) = id"
      and "space Y = UNIV"
    shows "standard_borel_space_UNIV Y"
  using assms
  by(auto intro!: standard_borelI simp: standard_borel_space_UNIV_def standard_borel_space_UNIV_axioms_def)

lemma standard_borel_space_UNIVI':
  assumes "standard_borel Y"
      and "space Y = UNIV"
    shows "standard_borel_space_UNIV Y"
  using assms by(simp add: standard_borel_space_UNIV_def standard_borel_space_UNIV_axioms_def)

subsection ‹ $\mathbb{R}$, $\mathbb{N}$, Boolean, $[0,\infty]$ ›
text ‹ $\mathbb{R}$ is a standard Borel space. ›
interpretation real : standard_borel_space_UNIV "real_borel"
  by(auto intro!: standard_borel_space_UNIVI)  

text‹ A non-empty Borel subspace of $\mathbb{R}$ is also a standard Borel space. ›
lemma real_standard_borel_subset:
  assumes "U ∈ sets real_borel"
      and "U ≠ {}"
    shows "standard_borel (restrict_space real_borel U)"
proof -
  have std1: "id ∈ (restrict_space real_borel U) →⇩M real_borel"
    by (simp add: measurable_restrict_space1)
  obtain x where hx : "x ∈ U"
    using assms(2) by auto
  define g :: "real ⇒ real"
    where "g ≡ (λr. if r ∈ U then r else x)"
  have "g ∈ real_borel →⇩M real_borel"
    unfolding g_def by(rule borel_measurable_continuous_on_if) (simp_all add: assms(1))
  hence std2: "g ∈ real_borel →⇩M (restrict_space real_borel U)"
    by(auto intro!: measurable_restrict_space2 simp: g_def hx)
  have std3: "∀y∈ space (restrict_space real_borel U). (g ∘ id) y = y"
    by(simp add: g_def space_restrict_space)
  show ?thesis
    using std1 std2 std3 standard_borel_def by blast
qed

text ‹ A non-empty measurable subset of a standard Borel space is also a standard Borel space.›
lemma(in standard_borel) standard_borel_subset:
  assumes "U ∈ sets M"
          "U ≠ {}"
    shows "standard_borel (restrict_space M U)"
proof -
  let ?ginvU = "g -` U"
  have hgu1:"?ginvU ∈ sets real_borel"
    using assms(1) g_meas measurable_sets_borel by blast
  have hgu2:"f ` U ⊆ ?ginvU"
    using gf_comp_id sets.sets_into_space[OF assms(1)] by fastforce
  hence hgu3:"?ginvU ≠ {}"
    using assms(2) by blast
  interpret r_borel_set: standard_borel "restrict_space real_borel ?ginvU"
    by(rule real_standard_borel_subset[OF hgu1 hgu3])
 
  have std1: "r_borel_set.f ∘ f ∈ (restrict_space M U) →⇩M real_borel"
    using sets.sets_into_space[OF assms(1)]
    by(auto intro!: measurable_comp[where N="restrict_space real_borel ?ginvU"] measurable_restrict_space3)
  have std2: "g ∘ r_borel_set.g ∈ real_borel →⇩M (restrict_space M U)"
    by(auto intro!: measurable_comp[where N="restrict_space real_borel ?ginvU"] measurable_restrict_space3[OF g_meas])
  have std3: "∀x∈ space (restrict_space M U). ((g ∘ r_borel_set.g) ∘ (r_borel_set.f ∘ f)) x = x"
    by (simp add: space_restrict_space)
  show ?thesis
    using std1 std2 std3 standard_borel_def by blast
qed

text ‹ $\mathbb{N}$ is a standard Borel space. ›
interpretation nat : standard_borel_space_UNIV nat_borel
proof -
  define n_to_r :: "nat ⇒ real"
    where "n_to_r ≡ (λn. of_real n)"
  define r_to_n :: "real ⇒ nat"
    where "r_to_n ≡ (λr. nat ⌊r⌋)"

  have n_to_r_measurable: "n_to_r ∈ nat_borel →⇩M real_borel"
    using borel_measurable_count_space measurable_cong_sets sets_borel_eq_count_space
    by blast
  have r_to_n_measurable: "r_to_n ∈ real_borel →⇩M nat_borel"
    by(simp add: r_to_n_def)
  have n_to_r_to_n_id: "r_to_n ∘ n_to_r = id"
    by(simp add: n_to_r_def r_to_n_def comp_def id_def)
  show "standard_borel_space_UNIV nat_borel"
    using standard_borel_space_UNIVI[OF n_to_r_measurable r_to_n_measurable n_to_r_to_n_id]
    by simp
qed

text ‹ For a countable space $X$, $X$ is a standard Borel space iff $X$ is a discrete space. ›
lemma countable_standard_iff:
  assumes "space X ≠ {}"
      and "countable (space X)"
  shows "standard_borel X ⟷ sets X = sets (count_space (space X))"
proof
  show "standard_borel X ⟹ sets X = sets (count_space (space X))"
    using standard_borel.countable_space_discrete assms by simp
next
  assume h[measurable_cong]: "sets X = sets (count_space (space X))"
  show "standard_borel X"
  proof(rule standard_borelI[where f="nat.f ∘ to_nat_on (space X)" and g="from_nat_into (space X) ∘ nat.g"])
    show "nat.f ∘ to_nat_on (space X) ∈ borel_measurable X"
      by simp
  next
    have [simp]: "from_nat_into (space X) ∈ UNIV → (space X)"
      using from_nat_into[OF assms(1)] by simp
    hence [measurable]: "from_nat_into (space X) ∈ nat_borel →⇩M X"
      using measurable_count_space_eq1[of _ _ X] measurable_cong_sets[OF sets_borel_eq_count_space]
      by blast
    show "from_nat_into (space X) ∘ nat.g ∈ real_borel →⇩M X"
      by simp
  next
    fix x
    assume "x ∈ space X"
    then show "(from_nat_into (space X) ∘ nat.g ∘ (nat.f ∘ to_nat_on (space X))) x = x"
      using from_nat_into_to_nat_on[OF assms(2)] by simp
  qed
qed

text ‹ $\mathbb{B}$ is a standard Borel space. ›
lemma to_bool_measurable:
  assumes "f -` {True} ∩ space M  ∈ sets M"
  shows "f ∈ M →⇩M bool_borel"
proof(rule measurableI)
  fix A
  assume h:"A ∈ sets bool_borel"
  have h2: "f -` {False} ∩ space M  ∈ sets M"
  proof -
    have "- {False} = {True}"
      by auto
    thus ?thesis
      by(simp add: vimage_sets_compl_iff[where A="{False}"] assms)
  qed
  have "A ⊆ {True,False}"
    by auto
  then consider "A = {}" | "A = {True}" | "A = {False}" | "A = {True,False}"
    by auto
  thus "f -` A ∩ space M ∈ sets M"
  proof cases
    case 1
    then show ?thesis
      by simp
  next
    case 2
    then show ?thesis
      by(simp add: assms)
  next
    case 3
    then show ?thesis
      by(simp add: h2)
  next
    case 4
    then have "f -` A = f -` {True} ∪ f -` {False}"
      by auto
    thus ?thesis
      using assms h2
      by (metis Int_Un_distrib2 sets.Un)
  qed
qed simp

interpretation bool : standard_borel_space_UNIV bool_borel
  using countable_standard_iff[of bool_borel]
  by(auto intro!: standard_borel_space_UNIVI' simp: sets_borel_eq_count_space)


text ‹ $[0,\infty]$ (the set of extended non-negative real numbers) is a standard Borel space.  ›
interpretation ennreal : standard_borel_space_UNIV ennreal_borel
proof -
  define preal_to_real :: "ennreal ⇒ real"
    where "preal_to_real ≡ (λr. if r = ∞ then -1
                                           else enn2real r)"
  define real_to_preal :: "real ⇒ ennreal"
    where "real_to_preal ≡ (λr. if r = -1 then ∞
                                          else ennreal r)"
  have preal_to_real_measurable: "preal_to_real ∈ ennreal_borel →⇩M real_borel"
    unfolding preal_to_real_def by simp
  have real_to_preal_measurable: "real_to_preal ∈ real_borel →⇩M ennreal_borel"
    unfolding real_to_preal_def by simp
  have preal_real_preal_id: "real_to_preal ∘ preal_to_real = id"
  proof
    fix r :: ennreal
    show "(real_to_preal ∘ preal_to_real) r = id r"
      using ennreal_enn2real_if[of r] ennreal_neg
      by(auto simp add: real_to_preal_def preal_to_real_def)
  qed
  show "standard_borel_space_UNIV ennreal_borel"
    using standard_borel_space_UNIVI[OF preal_to_real_measurable real_to_preal_measurable preal_real_preal_id]
    by simp
qed

subsection ‹ $\mathbb{R}\times\mathbb{R}$ ›
definition real_to_01open :: "real ⇒ real" where
"real_to_01open r ≡ arctan r / pi + 1 / 2"

definition real_to_01open_inverse :: "real ⇒ real" where
"real_to_01open_inverse r ≡ tan (pi * r - (pi / 2))"

lemma real_to_01open_inverse_correct:
 "real_to_01open_inverse ∘ real_to_01open = id"
  by(auto simp add: real_to_01open_def real_to_01open_inverse_def distrib_left tan_arctan)

lemma real_to_01open_inverse_correct':
  assumes "0 < r" "r < 1"
  shows "real_to_01open (real_to_01open_inverse r) = r"
  unfolding real_to_01open_def real_to_01open_inverse_def
proof -
  have "arctan (tan (pi * r - pi / 2)) = pi * r - pi / 2"
    using  arctan_unique[of "pi * r - pi / 2"] assms
    by simp
  hence "arctan (tan (pi * r - pi / 2)) / pi + 1 / 2 = ((pi * r) - pi / 2)/ pi + 1/2"
    by simp
  also have "... = r - 1/2 + 1/2"
    by (metis (no_types, opaque_lifting) divide_inverse mult.left_neutral nonzero_mult_div_cancel_left pi_neq_zero right_diff_distrib)
  finally show "arctan (tan (pi * r - pi / 2)) / pi + 1 / 2 = r"
    by simp
qed

lemma real_to_01open_01 :
 "0 < real_to_01open r ∧ real_to_01open r < 1"
proof
  have "- pi / 2 < arctan r" by(simp add: arctan_lbound)
  hence "0 < arctan r + pi / 2" by simp
  hence "0 < (1 / pi) * (arctan r + pi / 2)" by simp
  thus "0 < real_to_01open r"
    by (simp add: add_divide_distrib real_to_01open_def)
next
  have "arctan r < pi / 2" using arctan_ubound by simp
  hence "arctan r + pi / 2 < pi" by simp
  hence "(1 / pi) * (arctan r + pi / 2) < 1" by simp
  thus "real_to_01open r < 1"
    by(simp add: real_to_01open_def add_divide_distrib)
qed

lemma real_to_01open_continuous:
 "continuous_on UNIV real_to_01open"
proof -
  have "continuous_on UNIV ((λx. x / pi + 1 / 2) ∘ arctan)"
  proof (rule continuous_on_compose)
    show "continuous_on UNIV arctan"
      by (simp add: continuous_on_arctan)
  next
    show "continuous_on (range arctan) (λx. x / pi + 1 / 2)"
      by(auto intro!: continuous_on_add continuous_on_divide)
  qed
  thus ?thesis
    by(simp add: real_to_01open_def)
qed

lemma real_to_01open_inverse_continuous:
 "continuous_on {0<..<1} real_to_01open_inverse"
  unfolding real_to_01open_inverse_def
proof(rule Transcendental.continuous_on_tan)
  have [simp]: "(λx. pi * x - pi / 2) = (λx. x - pi/2) ∘ (λx. pi * x)"
    by auto
  have "continuous_on {0<..<1} ..."
  proof(rule continuous_on_compose)
    show "continuous_on {0<..<1} ((*) pi)"
      by simp
  next
    show "continuous_on ((*) pi ` {0<..<1}) (λx. x - pi / 2)"
      using continuous_on_diff[of "(*) pi ` {0<..<1}" "λx. x"]
      by simp
  qed
  thus "continuous_on {0<..<1} (λx. pi * x - pi / 2)" by simp
next
  have "∀r∈{0<..<1::real}. -(pi/2) < pi * r - pi / 2 ∧ pi * r - pi / 2 < pi/2"
    by simp
  thus "∀r∈{0<..<1::real}. cos (pi * r - pi / 2) ≠ 0"
    using cos_gt_zero_pi by fastforce
qed

lemma real_to_01open_inverse_measurable:
 "real_to_01open_inverse ∈ restrict_space real_borel {0<..<1} →⇩M real_borel"
  using borel_measurable_continuous_on_restrict real_to_01open_inverse_continuous
  by simp

fun r01_binary_expansion'' :: "real ⇒ nat ⇒ nat × real × real" where
"r01_binary_expansion'' r 0 = (if 1/2 ≤ r then (1,1  ,1/2)
                                            else (0,1/2,  0))" |
"r01_binary_expansion'' r (Suc n) = (let (_,ur,lr) = r01_binary_expansion'' r n;
                                           k = (ur + lr)/2 in
                                           (if k ≤ r then (1,ur,k)
                                                     else (0,k,lr)))"


text ‹ $a_n$  where $r = 0.a_0 a_1 a_2 ....$ for $0 < r < 1$.›
definition r01_binary_expansion' :: "real ⇒ nat ⇒ nat" where
"r01_binary_expansion' r n ≡ fst (r01_binary_expansion'' r n)"

text ‹$a_n = 0$ or $1$.›
lemma real01_binary_expansion'_0or1:
  "r01_binary_expansion' r n ∈ {0,1}"
  by (cases n) (simp_all add: r01_binary_expansion'_def split_beta' Let_def)

(* S_n = a_0 + ... + a_n *)
definition r01_binary_sum :: "(nat ⇒ nat) ⇒ nat ⇒ real" where
"r01_binary_sum a n ≡ (∑i=0..n. real (a i) * ((1/2)^(Suc i)))"

definition r01_binary_sum_lim :: "(nat ⇒ nat) ⇒ real" where
"r01_binary_sum_lim  ≡ lim ∘ r01_binary_sum" 


definition r01_binary_expression :: "real ⇒ nat ⇒ real" where
"r01_binary_expression ≡ r01_binary_sum ∘ r01_binary_expansion'"

lemma r01_binary_expansion_lr_r_ur:
  assumes "0 < r" "r < 1"
  shows "(snd (snd (r01_binary_expansion'' r n))) ≤ r ∧
         r < (fst (snd (r01_binary_expansion'' r n)))"
  using assms by (induction n) (simp_all add:split_beta' Let_def)

text ‹‹0 ≤ lr ∧ lr < ur ∧ ur ≤ 1›.›
lemma r01_binary_expansion_lr_ur_nn:
  shows "0 ≤ snd (snd (r01_binary_expansion'' r n)) ∧
         snd (snd (r01_binary_expansion'' r n)) < fst (snd (r01_binary_expansion'' r n)) ∧
         fst (snd (r01_binary_expansion'' r n)) ≤ 1"
  by (induction n) (simp_all add:split_beta' Let_def)

lemma r01_binary_expansion_diff:
  shows "(fst (snd (r01_binary_expansion'' r n))) - (snd (snd (r01_binary_expansion'' r n))) = (1/2)^(Suc n)"
proof(induction n)
  case (Suc n')
  then show ?case
  proof(cases "r01_binary_expansion'' r n'")
    case 1:(fields a ur lr)
    assume "fst (snd (r01_binary_expansion'' r n')) - snd (snd (r01_binary_expansion'' r n')) = (1 / 2) ^ (Suc n')"
    then have 2:"ur - lr = (1/2)^(Suc n')" by (simp add: 1)
    show ?thesis
    proof -
      have [simp]:"ur * 4 - (ur * 4 + lr * 4) / 2 = (ur - lr) * 2"
        by(simp add: division_ring_class.add_divide_distrib)
      have "ur * 4 - (ur * 4 + lr * 4) / 2 = (1 / 2) ^ n'"
        by(simp add: 2)
      moreover have "(ur * 4 + lr * 4) / 2 - lr * 4 = (1 / 2) ^ n'"
        by(simp add: division_ring_class.add_divide_distrib ring_class.right_diff_distrib[symmetric] 2)
      ultimately show ?thesis
        by(simp add: 1 Let_def)
    qed
  qed
qed simp

text ‹‹lrn = Sn›.›
lemma r01_binary_expression_eq_lr:
  "snd (snd (r01_binary_expansion'' r n)) = r01_binary_expression r n"
proof(induction n)
  case 0
  then show ?case
    by(simp add: r01_binary_expression_def r01_binary_sum_def r01_binary_expansion'_def)
next
  case 1:(Suc n')
  show ?case
  proof (cases "r01_binary_expansion'' r n'")
    case 2:(fields a ur lr)
    then have ih:"lr = (∑i = 0..n'. real (fst (r01_binary_expansion'' r i)) * (1 / 2) ^ i / 2)"
      using 1 by(simp add: r01_binary_expression_def r01_binary_sum_def r01_binary_expansion'_def)
    have 3:"(ur + lr) / 2 = lr + (1/2)^(Suc (Suc n'))"
      using r01_binary_expansion_diff[of r n'] 2 by simp
    show ?thesis
      by(simp add: r01_binary_expression_def r01_binary_sum_def r01_binary_expansion'_def 2 Let_def 3) fact
  qed
qed

lemma r01_binary_expression'_sum_range:
 "∃k::nat.  (snd (snd (r01_binary_expansion'' r n))) = real k/2^(Suc n) ∧
             k < 2^(Suc n) ∧
            ((r01_binary_expansion' r n) = 0 ⟶ even k) ∧
            ((r01_binary_expansion' r n) = 1 ⟶ odd k)"
proof -
  have [simp]:"(snd (snd (r01_binary_expansion'' r n))) = (∑i=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i)))"
    using r01_binary_expression_eq_lr[of r n] by(simp add: r01_binary_expression_def r01_binary_sum_def)
  have "∃k::nat. (∑i=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i))) = real k/2^(Suc n) ∧
             k < 2^(Suc n) ∧
            ((r01_binary_expansion' r n) = 0 ⟶ even k) ∧
            ((r01_binary_expansion' r n) = 1 ⟶ odd k)"
  proof(induction n)
    case 0
    consider "r01_binary_expansion' r 0 = 0" | "r01_binary_expansion' r 0 = 1"
      using real01_binary_expansion'_0or1[of r 0] by auto
    then show ?case
      by cases auto
  next
    case (Suc n')
    then obtain k :: nat where ih:
     "(∑i = 0..n'. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) = real k / 2^(Suc n') ∧ k < 2^(Suc n')"
      by auto
    have "(∑i = 0..Suc n'. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) = (∑i = 0..n'. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) + real (r01_binary_expansion' r (Suc n')) * (1 / 2) ^ Suc (Suc n')"
      by simp
    also have "... = real k / 2^(Suc n') + (real (r01_binary_expansion' r (Suc n')))/ 2^ Suc (Suc n')"
    proof -
      have "⋀r ra n. (r::real) * (1 / ra) ^ n = r / ra ^ n"
        by (simp add: power_one_over)
      then show ?thesis
        using ih by presburger
    qed
    also have "... = (2*real k) / 2^(Suc (Suc n')) + (real (r01_binary_expansion' r (Suc n')))/ 2^ Suc (Suc n')"
      by simp
    also have "... = (2*(real k) + real (r01_binary_expansion' r (Suc n')))/2 ^ Suc (Suc n')"
      by (simp add: add_divide_distrib)
    also have "... = (real (2*k + r01_binary_expansion' r (Suc n')))/2 ^ Suc (Suc n')"
      by simp
    finally have "(∑i = 0..Suc n'. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) = real (2 * k + r01_binary_expansion' r (Suc n')) / 2 ^ Suc (Suc n')" .
    moreover have "2 * k + r01_binary_expansion' r (Suc n') < 2^Suc (Suc n')"
    proof -
      have "k + 1 ≤ 2^Suc n'"
        using ih by simp
      hence "2*k + 2 ≤ 2^Suc (Suc n')"
        by simp
      thus ?thesis
        using real01_binary_expansion'_0or1[of r "Suc n'"]
        by auto
    qed
    moreover have "r01_binary_expansion' r (Suc n') = 0 ⟶ even (2 * k + r01_binary_expansion' r (Suc n'))"
      by simp
    moreover have "r01_binary_expansion' r (Suc n') = 1 ⟶ odd (2 * k + r01_binary_expansion' r (Suc n'))"
      by simp
    ultimately show ?case by fastforce
  qed
  thus ?thesis
    by simp
qed

text ‹‹an = bn ↔ Sn = S'n›.›
lemma r01_binary_expansion'_expression_eq:
  "r01_binary_expansion' r1 = r01_binary_expansion' r2 ⟷
   r01_binary_expression r1 = r01_binary_expression r2"
proof
  assume "r01_binary_expansion' r1 = r01_binary_expansion' r2"
  then show "r01_binary_expression r1 = r01_binary_expression r2"
    by(simp add: r01_binary_expression_def)
next
  assume "r01_binary_expression r1 = r01_binary_expression r2"
  then have 1:"⋀n. r01_binary_sum (r01_binary_expansion' r1) n = r01_binary_sum (r01_binary_expansion' r2) n"
    by(simp add: r01_binary_expression_def)
  show "r01_binary_expansion' r1 = r01_binary_expansion' r2"
  proof
    fix n
    show " r01_binary_expansion' r1 n = r01_binary_expansion' r2 n"
    proof(cases n)
      case 0
      then show ?thesis
        using 1[of 0] by(simp add: r01_binary_sum_def)
    next
      fix n'
      case (Suc n')
      have "r01_binary_sum (r01_binary_expansion' r1) n - r01_binary_sum (r01_binary_expansion' r1) n' = r01_binary_sum (r01_binary_expansion' r2) n - r01_binary_sum (r01_binary_expansion' r2) n'"
        by(simp add: 1)
      thus ?thesis
        using ‹n = Suc n'› by(simp add: r01_binary_sum_def)
    qed
  qed
qed

lemma power2_e:
 "⋀e::real. 0 < e ⟹ ∃n::nat. real_of_rat (1/2)^n < e"
  by (simp add: real_arch_pow_inv)

lemma r01_binary_expression_converges_to_r:
  assumes "0 < r"
     and  "r < 1"
   shows "LIMSEQ (r01_binary_expression r)  r"
proof
  fix e :: real
  assume "0 < e"
  then obtain k :: nat where hk:"real_of_rat (1/2)^k < e"
    using power2_e by auto
  show "∀⇩F x in sequentially. dist (r01_binary_expression r x) r < e"
  proof(rule eventually_sequentiallyI[of k])
    fix m
    assume "k ≤ m"
    have "¦ r - r01_binary_expression r m ¦ < e"
    proof (cases "r01_binary_expansion'' r m")
      case 1:(fields a ur lr)
      then have "¦r - r01_binary_expression r m¦ = ¦r - lr¦"
        by (metis r01_binary_expression_eq_lr snd_conv)
      also have "... = r - lr"
        using r01_binary_expansion_lr_r_ur[OF assms] 1        
        by (metis abs_of_nonneg diff_ge_0_iff_ge snd_conv)
      also have "... < e"
      proof -
        have "r - lr ≤ ur - lr"
          using r01_binary_expansion_lr_r_ur[of r] assms 1
          by (metis diff_right_mono fst_conv less_imp_le snd_conv)
        also have "... = (1/2)^(Suc m)"
          using r01_binary_expansion_diff[of r m]
          by(simp add: 1)
        also have "... ≤ (1/2)^(Suc k)"
          using ‹k ≤ m› by simp
        also have "... < (1/2)^k" by simp
        finally show ?thesis
          using hk by (simp add: of_rat_divide)
      qed
      finally show ?thesis .
    qed      
    then show "dist (r01_binary_expression r m) r < e"
      by (simp add: dist_real_def)
  qed
qed

lemma r01_binary_expression_correct:
  assumes "0 < r"
     and  "r < 1"
   shows "r = (∑n. real (r01_binary_expansion' r n) * (1/2)^(Suc n))"
proof -
  have "(λn. (λn. ∑i<n. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) (Suc n)) = r01_binary_expression r"
  proof -
    have "⋀n. {..<Suc n} = {0..n}" by auto
    thus ?thesis
      by(auto simp add: r01_binary_expression_def r01_binary_sum_def)
  qed
  hence "LIMSEQ (λn. ∑i<n. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i)  r"
    using r01_binary_expression_converges_to_r[OF assms] LIMSEQ_imp_Suc[of "λn. ∑i<n. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i" r]
    by simp
  thus ?thesis
    using suminf_eq_lim[of "λn. real (r01_binary_expansion' r n) * (1/2)^(Suc n)"] assms limI[of "(λn. ∑i<n. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i)" r]
    by simp
qed


text ‹‹S0 ≤ S1 ≤ S2 ≤ ...›.›
lemma binary_sum_incseq:
   "incseq (r01_binary_sum a)"
  by(simp add: incseq_Suc_iff r01_binary_sum_def)

lemma r01_eq_iff:
  assumes "0 < r1" "r1 < 1"
          "0 < r2" "r2 < 1"
    shows "r1 = r2 ⟷ r01_binary_expansion' r1 = r01_binary_expansion' r2"
proof auto
  assume "r01_binary_expansion' r1 = r01_binary_expansion' r2"
  then have 1:"r01_binary_expression r1 = r01_binary_expression r2"
    using r01_binary_expansion'_expression_eq[of r1 r2] by simp
  have "r1 = lim (r01_binary_expression r1)"
    using limI[of _ r1] r01_binary_expression_converges_to_r[of r1] assms(1,2)
    by simp
  also have "... = lim (r01_binary_expression r2)"
    by (simp add: 1)
  also have "... = r2"
    using limI[of _ r2] r01_binary_expression_converges_to_r[of r2] assms(3,4)
    by simp
  finally show "r1 = r2" .
qed

lemma power_half_summable:
 "summable (λn. ((1::real) / 2) ^ Suc n)"
  using power_half_series summable_def by blast


lemma binary_expression_summable:
   assumes "⋀n. a n ∈ {0,1 :: nat}"
   shows "summable (λn. real (a n) * (1/2)^(Suc n))"
proof -
  have "summable (λn::nat. ¦real (a n) * ((1::real) / (2::real)) ^ Suc n¦)"
  proof(rule summable_rabs_comparison_test[of "λn. real (a n) * (1/2)^(Suc n)" "λn. (1/2)^(Suc n)"])
    have "⋀n. ¦real (a n) * (1 / 2) ^ Suc n¦ ≤ (1 / 2)^(Suc n)"
    proof -
      fix n
      have "¦real (a n) * (1 / 2) ^ Suc n¦ = real (a n) * (1 / 2) ^ Suc n"
        using assms by simp
      also have "... ≤ (1 / 2) ^ Suc n"
      proof -
        consider "a n = 0" | "a n = 1"
          using assms by (meson insertE singleton_iff)
        then show ?thesis
          by(cases,auto)
      qed
      finally show "¦real (a n) * (1 / 2) ^ Suc n¦ ≤ (1 / 2)^(Suc n)" .
    qed
    thus "∃N. ∀n≥N. ¦real (a n) * (1 / 2) ^ Suc n¦ ≤ (1 / 2) ^ Suc n"
      by simp
  next
    show "summable (λn. ((1::real) / 2) ^ Suc n)"
      using power_half_summable by simp
  qed
  thus ?thesis by simp
qed

lemma binary_expression_gteq0:
  assumes "⋀n. a n ∈ {0,1 :: nat}"
  shows "0 ≤ (∑n. real (a (n + k)) * (1 / 2) ^ Suc (n + k))"
proof -
  have "(∑n. 0) ≤ (∑n. real (a (n + k)) * (1 / 2) ^ Suc (n + k))"
    using binary_expression_summable[of a] summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" k] suminf_le[of "λn. 0" "λn. real (a (n + k)) * (1 / 2) ^ Suc (n + k)"] assms
    by simp
  thus ?thesis by simp
qed

lemma binary_expression_leeq1:
  assumes "⋀n. a n ∈ {0,1 :: nat}"
  shows "(∑n. real (a (n + k)) * (1 / 2) ^ Suc (n + k)) ≤ 1"
proof -
  have "(∑n. real (a (n + k)) * (1 / 2) ^ Suc (n + k)) ≤ (∑n. (1/2)^(Suc n))"
  proof(rule suminf_le)
    fix n
    have 1:"real (a (n + k)) * (1 / 2) ^ Suc (n + k) ≤ (1 / 2) ^ Suc (n + k)"
      using assms[of "n+k"] by auto
    have 2:"((1::real) / 2) ^ Suc (n + k) ≤ (1 / 2) ^ Suc n"
      by simp
    show "real (a (n + k)) * (1 / 2) ^ Suc (n + k) ≤ (1 / 2) ^ Suc n"
      by(rule order.trans[OF 1 2])
  next
    show "summable (λn. real (a (n + k)) * (1 / 2) ^ Suc (n + k))"
      using binary_expression_summable[of a] summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" k] assms
      by simp
  next
    show "summable (λn. ((1::real) / 2) ^ Suc n)"
      using power_half_summable by simp
  qed
  thus ?thesis
    using power_half_series sums_unique by fastforce
qed

lemma binary_expression_less_than:
  assumes "⋀n. a n ∈ {0,1 :: nat}"
  shows "(∑n. real (a (n + k)) * (1 / 2) ^ Suc (n + k)) ≤ (∑n. (1 / 2) ^ Suc (n + k))"
proof(rule suminf_le)
  fix n
  show "real (a (n + k)) * (1 / 2) ^ Suc (n + k) ≤ (1 / 2) ^ Suc (n + k)"
    using assms[of "n + k"] by auto
next
  show "summable (λn. real (a (n + k)) * (1 / 2) ^ Suc (n + k))"
    using summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" k] binary_expression_summable[of a] assms
    by simp
next
  show "summable (λn. ((1::real) / 2) ^ Suc (n + k))"
    using power_half_summable summable_iff_shift[of "λn. ((1::real) / 2) ^ Suc n" k]
    by simp
qed

lemma lim_sum_ai:
  assumes "⋀n. a n ∈ {0,1 :: nat}"
  shows "lim (λn. (∑i=0..n. real (a i) * (1/2)^(Suc i))) = (∑n::nat. real (a n) * (1/2)^(Suc n))"
proof -
  have "⋀n::nat. {0..n} = {..n}" by auto
  hence "LIMSEQ (λn. ∑i=0..n. real (a i) * (1 / 2) ^ Suc i) (∑n. real (a n) * (1 / 2) ^ Suc n)"
    using summable_LIMSEQ'[of "λn. real (a n) * (1/2)^(Suc n)"] binary_expression_summable[of a] assms
    by simp
  thus "lim (λn. (∑i=0..n. real (a i) * (1/2)^(Suc i))) = (∑n. real (a n) * (1 / 2) ^ Suc n)"
    using limI by simp
qed

lemma half_1_minus_sum:
 "1 - (∑i<k. ((1::real) / 2) ^ Suc i) = (1/2)^k"
  by(induction k) auto

lemma half_sum:
  "(∑n. ((1::real) / 2) ^ (Suc (n + k))) = (1/2)^k"
  using suminf_split_initial_segment[of "λn. ((1::real) / 2) ^ (Suc n)" k] half_1_minus_sum[of k] power_half_series sums_unique[of "λn. (1 / 2) ^ Suc n" 1] power_half_summable
  by fastforce

lemma ai_exists0_less_than_sum:
  assumes "⋀n. a n ∈ {0,1}"
          "i ≥ m"
      and "a i = 0"
    shows "(∑n::nat. real (a (n + m)) * (1/2)^(Suc (n + m))) < (1 / 2) ^ m"
proof -
  have "(∑n::nat. real (a (n + m)) * (1/2)^(Suc (n + m))) = (∑n<i-m. real (a (n + m)) * (1/2)^(Suc (n + m))) + (∑n::nat. real (a (n + i)) * (1/2)^(Suc (n + i)))"
    using suminf_split_initial_segment[of "λn. real (a (n + m)) * (1/2)^(Suc (n + m))" "i-m"] assms(1) binary_expression_summable[of a] summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" m] assms(2)
    by simp
  also have "... < (1 / 2) ^ m"
  proof -
    have "(∑n. real (a (n + i)) * (1 / 2) ^ Suc (n + i)) ≤ (1 / 2) ^ Suc i"
    proof -
      have "(∑n::nat. real (a (n + i)) * (1/2)^(Suc (n + i))) = (∑n::nat. real (a (Suc n + i)) * (1/2)^(Suc (Suc n + i)))"
        using suminf_split_head[of "λn. real (a (n + i)) * (1/2)^(Suc (n + i))"] assms(1,3) binary_expression_summable[of a] summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" i]
        by simp
      also have "... = (∑n::nat. real (a (n + Suc i)) * (1/2)^(Suc n + Suc i))"
        by simp
      also have "... ≤ (∑n::nat. (1/2)^(Suc n + Suc i))"
        using binary_expression_less_than[of a "Suc i"] assms(1)
        by simp
      also have "... = (1/2)^(Suc i)"
        using half_sum[of "Suc i"] by simp
      finally show ?thesis .
    qed
    moreover have "(∑n<i - m. real (a (n + m)) * (1 / 2) ^ Suc (n + m)) ≤ (1/2)^m - (1/2)^i"
    proof -
      have "(∑n<i - m. real (a (n + m)) * (1 / 2) ^ Suc (n + m)) ≤ (∑n<i - m. (1 / 2) ^ Suc (n + m))"
      proof -
        have "real (a i) * (1 / 2) ^ Suc i ≤ (1 / 2) ^ Suc i" for i
          using assms(1)[of i] by auto
        thus ?thesis
          by (simp add: sum_mono)
      qed
      also have "... = (∑n. (1 / 2) ^ Suc (n + m)) - (∑n. (1 / 2) ^ Suc (n + (i - m) + m))"
        using suminf_split_initial_segment[of "λn. (1 / 2) ^ Suc (n + m)" "i-m"] power_half_summable summable_iff_shift[of "λn. ((1::real) / 2) ^ Suc n" m]
        by fastforce
      also have "... = (∑n. (1 / 2) ^ Suc (n + m)) - (∑n. (1 / 2) ^ Suc (n + i))"
        using assms(2) by simp
      also have "... = (1/2)^m - (1/2)^i"
        using half_sum by fastforce
      finally show ?thesis .
    qed
    ultimately have "(∑n<i - m. real (a (n + m)) * (1 / 2) ^ Suc (n + m)) + (∑n. real (a (n + i)) * (1 / 2) ^ Suc (n + i)) ≤ (1 / 2) ^ Suc i + (1 / 2) ^ m - (1 / 2) ^ i"
      by linarith
    also have "... < (1 / 2) ^ m "
      by simp
    finally show ?thesis .
  qed
  finally show ?thesis .
qed

lemma ai_exists0_less_than1:
  assumes "⋀n. a n ∈ {0,1}"
      and "∃i. a i = 0"
    shows "(∑n::nat. real (a n) * (1/2)^(Suc n)) < 1"
  using ai_exists0_less_than_sum[of a 0] assms
  by auto

lemma ai_1_gt:
  assumes "⋀n. a n ∈ {0,1}"
      and "a i = 1"
    shows "(1/2)^(Suc i) ≤ (∑n::nat. real (a (n+i)) * (1/2)^(Suc (n+i)))"
proof -
  have 1:"(∑n::nat. real (a (n+i)) * (1/2)^(Suc (n+i))) = (1 / 2) ^ Suc (0 + i) + (∑n. real (a (Suc n + i)) * (1 / 2) ^ Suc (Suc n + i))"
    using suminf_split_head[of "λn. real (a (n+i)) * (1/2)^(Suc (n+i))"] binary_expression_summable[of a] summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" i] assms
    by simp
  show ?thesis
    using 1 binary_expression_gteq0[of a "Suc i"] assms(1)
    by simp
qed

lemma ai_exists1_gt0:
  assumes "⋀n. a n ∈ {0,1}"
      and "∃i. a i = 1"
    shows "0 < (∑n::nat. real (a n) * (1/2)^(Suc n))"
proof -
  obtain k where h1: "a k = 1"
    using assms(2) by auto
  have "(1/2)^(Suc k) = (∑n::nat. (if n = k then (1/2)^(Suc k) else (0::real)))"
  proof -
    have "(λn. if n ∈ {k} then (1 / 2) ^ Suc k else (0::real)) = (λn. if n = k then (1/2)^(Suc k) else 0)"
      by simp
    moreover have "(λn. if n ∈ {k} then (1 / 2) ^ Suc k else (0::real)) sums (∑r∈{k}. (1 / 2) ^ Suc k)"
      using sums_If_finite_set[of "{k}" "λn. ((1::real)/2)^(Suc k)"] by simp
    ultimately have "(λn. if n = k then (1 / 2) ^ Suc k else (0::real)) sums (1/2)^(Suc k)"
      by simp
    thus ?thesis
      using sums_unique[of "λn. if n = k then (1 / 2) ^ Suc k else (0::real)" "(1/2)^(Suc k)"]
      by simp
  qed
  also have "(∑n::nat. (if n = k then (1/2)^(Suc k) else 0)) ≤ (∑n::nat. real (a n) * (1/2)^(Suc n))"
  proof(rule suminf_le)
    show "⋀n. (if n = k then (1 / 2) ^ Suc k else 0) ≤ real (a n) * (1 / 2) ^ Suc n"
    proof -
      fix n
      show "(if n = k then (1 / 2) ^ Suc k else 0) ≤ real (a n) * (1 / 2) ^ Suc n"
        by(cases "n = k"; simp add: h1)
    qed
  next
    show "summable (λn. if n = k then (1 / 2) ^ Suc k else (0::real))"
      using summable_single[of k "λn. ((1::real) / 2) ^ Suc k"]
      by simp
  next
    show "summable (λn. real (a n) * (1 / 2) ^ Suc n)"
      using binary_expression_summable[of a] assms(1)
      by simp
  qed
  finally have "(1 / 2) ^ Suc k ≤ (∑n. real (a n) * (1 / 2) ^ Suc n)" .
  moreover have "0 < ((1::real) / 2) ^ Suc k" by simp
  ultimately show ?thesis by linarith
qed


lemma r01_binary_expression_ex0:
  assumes "0 < r" "r < 1"
  shows "∃i.  r01_binary_expansion' r i = 0"
proof (rule ccontr)
  assume "¬ (∃ i. r01_binary_expansion' r i = 0)"
  then have "⋀i. r01_binary_expansion' r i = 1"
    using real01_binary_expansion'_0or1[of r] by blast
  hence 1:"r01_binary_expression r = (λn. ∑i=0..n. ((1/2)^(Suc i)))"
    by(auto simp: r01_binary_expression_def r01_binary_sum_def)
  have "LIMSEQ (r01_binary_expression r)  1"
  proof -
    have "LIMSEQ (λn. ∑i=0..n. (((1::real)/2)^(Suc i))) 1"
      using power_half_series sums_def'[of "λn. ((1::real)/2)^(Suc n)" 1]
      by simp
    thus ?thesis
      using 1 by simp
  qed
  moreover have "LIMSEQ (r01_binary_expression r) r"
    using r01_binary_expression_converges_to_r[of r] assms
    by simp
  ultimately have "r = 1"
    using LIMSEQ_unique by auto
  thus False
    using assms by simp
qed

lemma r01_binary_expression_ex1:
  assumes "0 < r" "r < 1"
  shows "∃i.  r01_binary_expansion' r i = 1"
proof (rule ccontr)
  assume "¬ (∃i. r01_binary_expansion' r i = 1)"
  then have "⋀i. r01_binary_expansion' r i = 0"
    using real01_binary_expansion'_0or1[of r] by blast
  hence 1:"r01_binary_expression r = (λn. ∑i=0..n. 0)"
    by(auto simp add: r01_binary_expression_def r01_binary_sum_def)
  hence "LIMSEQ (r01_binary_expression r) 0"
    by simp
  moreover have "LIMSEQ (r01_binary_expression r) r"
    using r01_binary_expression_converges_to_r[of r] assms
    by simp
  ultimately have "r = 0"
    using LIMSEQ_unique by auto
  thus False
    using assms by simp
qed

lemma r01_binary_expansion'_gt1:
  "1 ≤ r ⟷ (∀n. r01_binary_expansion' r n = 1)"
proof auto
  fix n
  assume h:"1 ≤ r"
  show "r01_binary_expansion' r n = Suc 0"
    unfolding r01_binary_expansion'_def
  proof(cases n)
    case 0
    then show "fst (r01_binary_expansion'' r n) = Suc 0"
      using h by simp
  next
    case 2:(Suc n')
    show "fst (r01_binary_expansion'' r n) = Suc 0"
    proof(cases "r01_binary_expansion'' r n'")
      case 3:(fields a ur lr)
      then have "(ur + lr) / 2 ≤ 1"
        using r01_binary_expansion_lr_ur_nn[of r "Suc n'"]
        by (cases "((ur + lr) / 2) ≤ r") (auto simp: Let_def) 
      thus "fst (r01_binary_expansion'' r n) = Suc 0"
        using h by(simp add: 2 3 Let_def)
    qed
  qed
next
  assume h:"∀n. r01_binary_expansion' r n = Suc 0"
  show "1 ≤ r"
  proof(rule ccontr)
    assume "¬ 1 ≤ r"
    then consider "r ≤ 0" | "0 < r ∧ r < 1"
      by linarith
    then show "False"
    proof cases
      case 1
      then have "r01_binary_expansion' r 0 = 0"
        by(simp add: r01_binary_expansion'_def)
      then show ?thesis
        using h by simp
    next
      case 2
      then have "∃i.  r01_binary_expansion' r i = 0"
        using r01_binary_expression_ex0[of r] by simp
      then show ?thesis
        using h by simp
    qed
  qed
qed

lemma r01_binary_expansion'_lt0:
 "r ≤ 0 ⟷ (∀n. r01_binary_expansion' r n = 0)"
proof auto
  fix n
  assume h:"r ≤ 0"
  show "r01_binary_expansion' r n = 0"
  proof(cases n)
    case 0
    then show ?thesis
      using h by(simp add: r01_binary_expansion'_def)
  next
    case hn:(Suc n')
    then show ?thesis
      unfolding r01_binary_expansion'_def
    proof(cases "r01_binary_expansion'' r n'")
      case 1:(fields a ur lr)
      then have "0 < ((ur + lr) / 2)"
        using r01_binary_expansion_lr_ur_nn[of r n']
        by simp
      hence "r < ..."
        using h by linarith       
      then show "fst (r01_binary_expansion'' r n) = 0 "
        by(simp add: 1 hn Let_def)
    qed
  qed
next
  assume h:"∀n. r01_binary_expansion' r n = 0"
  show "r ≤ 0"
  proof(rule ccontr)
    assume "¬ r ≤ 0"
    then consider "0 < r ∧ r < 1" | "1 ≤ r" by linarith
    thus False
    proof cases
      case 1
      then have "∃i. r01_binary_expansion' r i = 1"
        using r01_binary_expression_ex1[of r] by simp
      then show ?thesis
        using h by simp
    next
      case 2
      then show ?thesis
        using r01_binary_expansion'_gt1[of r] h by simp
    qed
  qed
qed
    

text ‹The sequence $111111\dots$ does not appear in $r = 0.a_1 a_2\dots$. ›
lemma r01_binary_expression_ex0_strong:
  assumes "0 < r" "r < 1"
  shows "∃i≥n. r01_binary_expansion' r i = 0"
proof(cases "r01_binary_expansion'' r n")
  case 1:(fields a ur lr)
  show ?thesis
  proof(rule ccontr)
    assume "¬ (∃i≥n. r01_binary_expansion' r i = 0)"
    then have h:"∀i≥n. r01_binary_expansion' r i = 1"
      using real01_binary_expansion'_0or1[of r] by blast
    
    have "r = (∑i=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i))) + (∑i::nat. real (r01_binary_expansion' r (i + (Suc n))) * ((1/2)^(Suc (i + (Suc n)))))"
    proof -
      have "r = (∑l. real (r01_binary_expansion' r l) * (1 / 2) ^ Suc l)"
        using r01_binary_expression_correct[of r] assms by simp
      also have "... = (∑l. real (r01_binary_expansion' r (l + Suc n)) * (1 / 2) ^ Suc (l + Suc n)) + (∑i<Suc n. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i)"
        apply(rule suminf_split_initial_segment)
        apply(rule binary_expression_summable)
        using real01_binary_expansion'_0or1[of r] by simp
      also have "... = (∑i=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i))) + (∑i::nat. real (r01_binary_expansion' r (i + (Suc n))) * ((1/2)^(Suc (i + (Suc n)))))"
      proof -
        have "⋀n. {..<Suc n} = {0..n}" by auto
        thus ?thesis by simp
      qed
      finally show ?thesis .
    qed
    also have "... = (∑i=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i))) + (∑i::nat. ((1/2)^(Suc (i + (Suc n)))))"
      using h by simp
    also have "... = (∑i=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i))) + (1/2)^(Suc n)"
      using half_sum[of "Suc n"] by simp
    also have "... = lr + (1/2)^(Suc n)"
      using 1 r01_binary_expression_eq_lr[of r n]
      by(simp add: r01_binary_expression_def r01_binary_sum_def)
    also have "... = ur"
      using r01_binary_expansion_diff[of r n]
      by(simp add: 1)
    finally have "r = ur" .
    moreover have "r < ur"
      using r01_binary_expansion_lr_r_ur[of r n] assms 1
      by simp
    ultimately show False
      by simp
  qed
qed

text ‹ A binary expression is well-formed when $111\dots$ does not appear in the tail of the sequence ›
definition biexp01_well_formed :: "(nat ⇒ nat) ⇒ bool" where
"biexp01_well_formed a ≡ (∀n. a n ∈ {0,1}) ∧ (∀n. ∃m≥n. a m = 0)"

lemma biexp01_well_formedE:
  assumes "biexp01_well_formed a"
  shows "(∀n. a n ∈ {0,1}) ∧ (∀n. ∃m≥n. a m = 0)"
  using assms by(simp add: biexp01_well_formed_def)

lemma biexp01_well_formedI:
  assumes "⋀n. a n ∈ {0,1}"
      and "⋀n. ∃m≥n. a m = 0"
    shows "biexp01_well_formed a"
  using assms by(simp add: biexp01_well_formed_def)

lemma r01_binary_expansion_well_formed:
  assumes "0 < r" "r < 1"
  shows "biexp01_well_formed (r01_binary_expansion' r)"
  using r01_binary_expression_ex0_strong[of r] assms real01_binary_expansion'_0or1[of r]
  by(simp add: biexp01_well_formed_def)

lemma biexp01_well_formed_comb:
  assumes "biexp01_well_formed a"
      and "biexp01_well_formed b"
    shows "biexp01_well_formed (λn. if even n then a (n div 2)
                                              else b ((n-1) div 2))"
proof(rule biexp01_well_formedI)
  show "⋀n. (if even n then a (n div 2) else b ((n - 1) div 2)) ∈ {0, 1}"
    using assms biexp01_well_formedE by simp
next
  fix n
  obtain m where 1:"m≥n ∧ a m = 0"
    using assms biexp01_well_formedE by blast
  then have "a ((2*m) div 2) = 0" by simp
  hence "(if even (2*m) then a (2*m div 2) else b ((2*m - 1) div 2)) = 0"
    by simp
  moreover have "2*m ≥ n" using 1 by simp
  ultimately show "∃m≥n. (if even m then a (m div 2) else b ((m - 1) div 2)) = 0"
    by auto
qed



lemma nat_complete_induction:
  assumes "P (0 :: nat)"
      and "⋀n. (⋀m. m ≤ n ⟹ P m) ⟹ P (Suc n)"
    shows "P n"
proof(cases n)
  case 0
  then show ?thesis
    using assms(1) by simp
next
  case h:(Suc n')
  have "P (Suc n')"
  proof(rule assms(2))
    show "⋀m. m ≤ n' ⟹ P m"
    proof(induction n')
      case 0
      then show ?case
        using assms(1) by simp
    next
      case (Suc n'')
      then show ?case
        by (metis assms(2) le_SucE)
    qed
  qed
  thus ?thesis
    using h by simp
qed

text ‹ ‹(∑m. real (a m) * (1 / 2) ^ Suc m) n = a n›.›
lemma biexp01_well_formed_an:
  assumes "biexp01_well_formed a"
  shows "r01_binary_expansion' (∑m. real (a m) * (1 / 2) ^ Suc m) n = a n"
proof(rule nat_complete_induction[of _ n])
  show "r01_binary_expansion' (∑m. real (a m) * (1 / 2) ^ Suc m) 0 = a 0"
  proof (auto simp add: r01_binary_expansion'_def)
    assume h:"1 ≤ (∑m. real (a m) * (1 / 2) ^ m / 2) * 2"
    show "Suc 0 = a 0"
    proof(rule ccontr)
      assume "Suc 0 ≠ a 0"
      then have "a 0 = 0"
        using assms(1) biexp01_well_formedE[of a] by auto
      hence "(∑m. real (a m) * (1 / 2) ^ (Suc m)) = (∑m. real (a (Suc m)) * (1 / 2) ^ (Suc (Suc m)))"
        using suminf_split_head[of "λm. real (a m) * (1 / 2) ^ (Suc m)"] binary_expression_summable[of a] assms biexp01_well_formedE
        by simp
      also have "... < 1/2"
        using ai_exists0_less_than_sum[of a 1] assms biexp01_well_formedE[of a]
        by auto
      finally have "(∑m. real (a m) * (1 / 2) ^ m / 2) < 1/2"
        by simp
      thus False
        using h by simp
    qed
  next
    assume h:"¬ 1 ≤ (∑m. real (a m) * (1 / 2) ^ m / 2) * 2"
    show "a 0 = 0"
    proof(rule ccontr)
      assume "a 0 ≠ 0"
      then have "a 0 = 1"
        using assms(1) biexp01_well_formedE[of a]
        by (meson insertE singletonD)
      hence "1/2 ≤ (∑m. real (a m) * (1 / 2) ^ (Suc m))"
        using ai_1_gt[of a 0] assms(1) biexp01_well_formedE[of a]
        by auto
      thus False
        using h by simp
    qed
  qed
next
  fix n :: nat
  assume ih:"(⋀m. m ≤ n ⟹ r01_binary_expansion' (∑m. real (a m) * (1 / 2) ^ Suc m) m = a m)"
  show "r01_binary_expansion' (∑m. real (a m) * (1 / 2) ^ Suc m) (Suc n) = a (Suc n)"
  proof(cases "r01_binary_expansion'' (∑m. real (a m) * (1 / 2) ^ Suc m) n")
    case h:(fields bn ur lr)
    then have hlr:"lr = (∑k=0..n. real (a k) * (1 / 2) ^ Suc k)"
      using r01_binary_expression_eq_lr[of "∑m. real (a m) * (1 / 2) ^ Suc m" n] ih
      by(simp add: r01_binary_expression_def r01_binary_sum_def)
    have hlr2:"(ur + lr) / 2 = lr + (1/2)^(Suc (Suc n))"
    proof -
      have "(ur + lr) / 2 = lr + (1/2)^(Suc (Suc n))"
        using r01_binary_expansion_diff[of "∑m. real (a m) * (1 / 2) ^ Suc m" n] h by simp
      show ?thesis
        by (simp add: ‹(ur + lr) / 2 = lr + (1 / 2) ^ Suc (Suc n)› of_rat_add of_rat_divide of_rat_power)
    qed
    show ?thesis
      using h
    proof(auto simp add: r01_binary_expansion'_def Let_def)
      assume h1: "(ur + lr) ≤ (∑m. real (a m) * (1 / 2) ^ m / 2) * 2"
      show "Suc 0 = a (Suc n)"
      proof(rule ccontr)
        assume "Suc 0 ≠ a (Suc n)"
        then have "a (Suc n) = 0"
          using assms(1) biexp01_well_formedE[of a] by auto
        have "(∑m. real (a m) * (1 / 2) ^ m / 2) < (∑k=0..n. real (a k) * (1 / 2) ^ Suc k) + (1/2)^(Suc (Suc n))"
        proof -
          have "(∑m. real (a m) * (1 / 2) ^ (Suc m)) = (∑k=0..n. real (a k) * (1 / 2) ^ Suc k) + (∑m. real (a (m+Suc n)) * (1 / 2) ^ Suc (m + Suc n))"
          proof -
            have "{0..n} = {..<Suc n}" by auto
            thus ?thesis
              using suminf_split_initial_segment[of "λm. real (a m) * (1 / 2) ^ (Suc m)" "Suc n"] binary_expression_summable[of a] assms(1) biexp01_well_formedE[of a]
              by simp
          qed
          also have "... = (∑k=0..n. real (a k) * (1 / 2) ^ Suc k) + (∑m. real (a (Suc m + Suc n)) * (1 / 2) ^ Suc (Suc m + Suc n))"
            using suminf_split_head[of "λm. real (a (m + Suc n)) * (1 / 2) ^ (Suc (m + Suc n))"] binary_expression_summable[of a] assms(1) biexp01_well_formedE[of a] Series.summable_iff_shift[of "λm. real (a m) * (1 / 2) ^ (Suc m)" "Suc n"] ‹a (Suc n) = 0›
            by simp
          also have "... = (∑k=0..n. real (a k) * (1 / 2) ^ Suc k) + (∑m. real (a (m + Suc (Suc n))) * (1 / 2) ^ Suc (m + Suc (Suc n)))"
            by simp
          also have "... < (∑k=0..n. real (a k) * (1 / 2) ^ Suc k) + (1/2)^Suc (Suc n)"
            using ai_exists0_less_than_sum[of a "Suc (Suc n)"] assms(1) biexp01_well_formedE[of a]
            by auto
          finally show ?thesis by simp
        qed
        thus False
          using h1 hlr2 hlr by simp
      qed
    next
      assume h2:"¬ ur + lr ≤ (∑m. real (a m) * (1 / 2) ^ m / 2) * 2"
      show "a (Suc n) = 0"
      proof(rule ccontr)
        assume "a (Suc n) ≠ 0"
        then have "a (Suc n) = 1"
          using biexp01_well_formedE[OF assms(1)]
          by (meson insertE singletonD)
        have "(∑k=0..n. real (a k) * (1 / 2) ^ Suc k) + (1/2)^(Suc (Suc n)) ≤ (∑m. real (a m) * (1 / 2) ^ m / 2)"
        proof -
          have "(∑m. real (a m) * (1 / 2) ^ (Suc m)) = (∑k=0..n. real (a k) * (1 / 2) ^ Suc k) + (∑m. real (a (m+Suc n)) * (1 / 2) ^ Suc (m + Suc n))"
          proof -
            have "{0..n} = {..<Suc n}" by auto
            thus ?thesis
              using suminf_split_initial_segment[of "λm. real (a m) * (1 / 2) ^ (Suc m)" "Suc n"] binary_expression_summable[of a] assms(1) biexp01_well_formedE[of a]
              by simp
          qed
          also have "... = (∑k=0..n. real (a k) * (1 / 2) ^ Suc k) + (∑m. real (a (Suc m + Suc n)) * (1 / 2) ^ Suc (Suc m + Suc n)) + (1 / 2) ^ Suc (Suc n)"
            using suminf_split_head[of "λm. real (a (m + Suc n)) * (1 / 2) ^ (Suc (m + Suc n))"] binary_expression_summable[of a] assms(1) biexp01_well_formedE[of a] Series.summable_iff_shift[of "λm. real (a m) * (1 / 2) ^ (Suc m)" "Suc n"] ‹a (Suc n) = 1›
            by simp
          also have "... = (∑k=0..n. real (a k) * (1 / 2) ^ Suc k) + (∑m. real (a (m + Suc (Suc n))) * (1 / 2) ^ Suc (m + (Suc (Suc n)))) + (1 / 2) ^ Suc (Suc n)"
            by simp
          also have "... ≥ (∑k=0..n. real (a k) * (1 / 2) ^ Suc k) + (1 / 2) ^ Suc (Suc n)"
            using binary_expression_gteq0[of a "Suc (Suc n)"] assms(1) biexp01_well_formedE[of a] by simp
          finally show ?thesis by simp
        qed
        thus False
          using h2 hlr2 hlr by simp
      qed
    qed
  qed
qed


lemma f01_borel_measurable:
  assumes "f -` {0::real} ∈ sets real_borel"
          "f -` {1} ∈ sets borel"
      and "⋀r::real. f r ∈ {0,1}"
    shows "f ∈ borel_measurable real_borel"
proof(rule measurableI)
  fix U :: "real set"
  assume "U ∈ sets borel"
  consider "1 ∈ U ∧ 0 ∈ U" | "1 ∈ U ∧ 0 ∉ U" | "1 ∉ U ∧ 0 ∈ U" | "1 ∉ U ∧ 0 ∉ U"
    by auto
  then show "f -` U ∩ space real_borel ∈ sets borel"
  proof cases
    case 1
    then have "f -` U = UNIV"
      using assms(3) by auto
    then show ?thesis by simp
  next
    case 2
    then have "f -` U = f -` {1}"
      using assms(3) by fastforce
    then show ?thesis
      using assms(2) by simp
  next
    case 3
    then have "f -` U = f -` {0}"
      using assms(3) by fastforce
    then show ?thesis
      using assms(1) by simp
  next
    case 4
    then have "f -` U = {}"
      using assms(3) by (metis all_not_in_conv insert_iff vimage_eq)
    then show ?thesis by simp
  qed
qed simp


lemma r01_binary_expansion'_measurable:
 "(λr. real (r01_binary_expansion' r n)) ∈ borel_measurable (borel :: real measure)"
proof -
  have "(λr. real (r01_binary_expansion' r n)) -`{0} ∈ sets borel ∧ (λr. real (r01_binary_expansion' r n)) -`{1} ∈ sets borel"
  proof -
    let ?A = "{..0::real} ∪ (⋃i∈{l::nat. l < 2^(Suc n) ∧ even l} . {i/2^(Suc n)..<(Suc i)/2^(Suc n)})"
    let ?B = "{1::real..} ∪ (⋃i∈{l::nat. l < 2^(Suc n) ∧ odd l} .  {i/2^(Suc n)..<(Suc i)/2^(Suc n)})"
    have "?A ∈ sets borel" by simp
    have "?B ∈ sets borel" by simp
    have hE:"?A ∩ ?B = {}"
    proof auto
      fix r :: real
      fix l :: nat
      assume h: "r ≤ 0"
                "odd l"
                "real l / (2 * 2 ^ n) ≤ r"
      then have "0 < l" by(cases l; auto)
      hence "0 < real l / (2 * 2 ^ n)" by simp
      thus False
        using h by simp
    next
      fix r :: real
      fix l :: nat
      assume h: "l < 2 * 2 ^ n"
                "even l"
                "1 ≤ r"
                "r < (1 + real l) / (2 * 2 ^ n)"
      then have "1 + real l ≤ 2 * 2 ^ n"
        by (simp add: nat_less_real_le)
      moreover have "1 + real l ≠ 2 * 2 ^ n"
        using h by auto
      ultimately have "1 + real l < 2 * 2 ^ n" by simp
      hence "(1 + real l) / (2 * 2 ^ n) < 1" by simp
      thus False using h by linarith
    next
      fix r :: real
      fix l1 l2 :: nat
      assume h: "even l1" "odd l2"
                "real l1 / (2 * 2 ^ n) ≤ r" "r < (1 + real l1) / (2 * 2 ^ n)"
                "real l2 / (2 * 2 ^ n) ≤ r" "r < (1 + real l2) / (2 * 2 ^ n)"
      then consider "l1 < l2" | "l2 < l1"  by fastforce
      thus False
      proof cases
        case 1
        then have "(1 + real l1) / (2 * 2 ^ n) ≤ real l2 / (2 * 2 ^ n)"
          by (simp add: frac_le)
        then show ?thesis
          using h by simp
      next
        case 2
        then have "(1 + real l2) / (2 * 2 ^ n) ≤ real l1 / (2 * 2 ^ n)"
          by (simp add: frac_le)
        then show ?thesis
          using h by simp
      qed
    qed
    have hU:"?A ∪ ?B = UNIV"
    proof
      show "?A ∪ ?B ⊆ UNIV" by simp
    next
      show "UNIV ⊆ ?A ∪ ?B"
      proof
        fix r :: real
        consider "r ≤ 0" | "0 < r ∧ r < 1" | "1 ≤ r" by linarith
        then show "r ∈ ?A ∪ ?B"
        proof cases
          case 1
          then show ?thesis by simp
        next
          case 2
          show ?thesis
          proof(cases "r01_binary_expansion'' r n")
            case hc:(fields a ur lr)
            then have hlu:"lr ≤ r ∧ r < ur"
              using 2 r01_binary_expansion_lr_r_ur[of r n] by simp
            obtain k :: nat where hk:
             "lr = real k / 2 ^ Suc n ∧ k < 2 ^ Suc n"
              using r01_binary_expression'_sum_range[of r n] hc
              by auto
            hence "ur = real (Suc k) / 2^Suc n"
              using r01_binary_expansion_diff[of r n] hc
              by (simp add: add_divide_distrib power_one_over)
            thus ?thesis
              using hlu hk by auto
          qed
        next
          case 3
          then show ?thesis by simp
        qed
      qed
    qed
    have hi1:"- ?A = ?B"
    proof -
      have "?B ⊆ - ?A"
        using hE by blast
      moreover have "-?A ⊆ ?B"
      proof -
        have "-(?A ∪ ?B) = {}"
          using hU by simp
        hence "(-?A) ∩ (-?B) = {}" by simp
        thus ?thesis
          by blast
      qed
      ultimately show ?thesis
        by blast
    qed
    have hi2: "?A = -?B"
      using hi1 by blast

    let ?U0 = "(λr. real (r01_binary_expansion' r n)) -`{0}"
    let ?U1 = "(λr. real (r01_binary_expansion' r n)) -`{1}"

    have hU':"?U0 ∪ ?U1 = UNIV"
    proof -
      have "?U0 ∪ ?U1 = (λr. real (r01_binary_expansion' r n)) -`{0,1}"
        by auto
      thus ?thesis
        using real01_binary_expansion'_0or1[of _ n] by auto
    qed
    have hE':"?U0 ∩ ?U1 = {}"
      by auto

    have hiu1:"- ?U0 = ?U1"
      using hE' hU' by fastforce

    have hiu2:"- ?U1 = ?U0"
      using hE' hU' by fastforce

    have "?U0 ⊆ ?A"
    proof
      fix r
      assume "r ∈ ?U0"
      then have h1:"r01_binary_expansion' r n = 0"
        by simp
      then consider "r ≤ 0" | "0 < r ∧ r < 1"
        using r01_binary_expansion'_gt1[of r] by fastforce
      thus "r ∈ ?A"
      proof cases
        case 1
        then show ?thesis by simp
      next
        case 2
        then have 3:"(snd (snd (r01_binary_expansion'' r n))) ≤ r ∧
                     r < (fst (snd (r01_binary_expansion'' r n)))"
          using r01_binary_expansion_lr_r_ur[of r n] by simp
        obtain k where 4: 
          "(snd (snd (r01_binary_expansion'' r n))) =
           real k / 2 ^ Suc n ∧
           k < 2 ^ Suc n ∧ even k"
          using r01_binary_expression'_sum_range[of r n] h1
          by auto
        have "(fst (snd (r01_binary_expansion'' r n))) = real (Suc k) / 2 ^ Suc n"
        proof -
          have "(fst (snd (r01_binary_expansion'' r n))) = (snd (snd (r01_binary_expansion'' r n))) + (1/2)^Suc n"
            using r01_binary_expansion_diff[of r n] by linarith
          thus ?thesis
            using 4
            by (simp add: add_divide_distrib power_one_over)
        qed
        thus ?thesis
          using 3 4 by auto
      qed
    qed

    have "?U1 ⊆ ?B"
    proof
      fix r
      assume "r ∈ ?U1"
      then have h1:"r01_binary_expansion' r n = 1"
        by simp
      then consider "1 ≤ r" | "0 < r ∧ r < 1"
        using r01_binary_expansion'_lt0[of r] by fastforce
      thus "r ∈ ?B"
      proof cases
        case 1
        then show ?thesis by simp
      next
        case 2
        then have 3:"(snd (snd (r01_binary_expansion'' r n))) ≤ r ∧
                     r < (fst (snd (r01_binary_expansion'' r n)))"
          using r01_binary_expansion_lr_r_ur[of r n] by simp
        obtain k where 4: 
          "(snd (snd (r01_binary_expansion'' r n))) =
           real k / 2 ^ Suc n ∧
           k < 2 ^ Suc n ∧ odd k"
          using StandardBorel.r01_binary_expression'_sum_range[of r n] h1
          by auto
        have "(fst (snd (r01_binary_expansion'' r n))) = real (Suc k) / 2 ^ Suc n"
        proof -
          have "(fst (snd (r01_binary_expansion'' r n))) = (snd (snd (r01_binary_expansion'' r n))) + (1/2)^Suc n"
            using r01_binary_expansion_diff[of r n] by simp
          thus ?thesis
            using 4
            by (simp add: add_divide_distrib power_one_over)
        qed
        thus ?thesis
          using 3 4 by auto
      qed
    qed

    have "?U0 = ?A"
    proof
      show "?U0 ⊆ ?A" by fact
    next
      show "?A ⊆ ?U0"
        using  ‹?U1 ⊆ ?B› Compl_subset_Compl_iff[of ?U0 ?A] hi1 hiu1
        by blast
    qed

    have "?U1 = ?B"
      using ‹?U0 = ?A› hi1 hiu1 by auto
    show ?thesis
      using ‹?U0 = ?A› ‹?U1 = ?B› ‹?A ∈ sets borel› ‹?B ∈ sets borel›
      by simp
  qed
  thus ?thesis
    using f01_borel_measurable[of "(λr. real (r01_binary_expansion' r n))"] real01_binary_expansion'_0or1[of _ n]
    by simp
qed



(* (0,1) ⇒ [0,1]×[0,1]. *)
definition r01_to_r01_r01_fst' :: "real ⇒ nat ⇒ nat" where
"r01_to_r01_r01_fst' r n ≡ r01_binary_expansion' r (2*n)"

lemma r01_to_r01_r01_fst'in01:
  "⋀n. r01_to_r01_r01_fst' r n ∈ {0,1}"
  using real01_binary_expansion'_0or1 by (simp add: r01_to_r01_r01_fst'_def)

definition r01_to_r01_r01_fst_sum :: "real ⇒ nat ⇒ real" where
"r01_to_r01_r01_fst_sum ≡ r01_binary_sum ∘ r01_to_r01_r01_fst'"

definition r01_to_r01_r01_fst :: "real ⇒ real" where
"r01_to_r01_r01_fst = lim ∘ r01_to_r01_r01_fst_sum"

lemma r01_to_r01_r01_fst_def':
  "r01_to_r01_r01_fst r = (∑n. real (r01_binary_expansion' r (2*n)) * (1/2)^(n+1))"
proof -
  have "r01_to_r01_r01_fst_sum r = (λn. ∑i=0..n. real (r01_binary_expansion' r (2*i)) * (1/2)^(i+1))"
    by(auto simp add: r01_to_r01_r01_fst_sum_def r01_binary_sum_def r01_to_r01_r01_fst'_def)
  thus ?thesis
    using lim_sum_ai real01_binary_expansion'_0or1
    by(simp add: r01_to_r01_r01_fst_def)
qed

lemma r01_to_r01_r01_fst_measurable:
 "r01_to_r01_r01_fst ∈ borel_measurable borel"
  unfolding r01_to_r01_r01_fst_def'
  using r01_binary_expansion'_measurable by auto


definition r01_to_r01_r01_snd' :: "real ⇒ nat ⇒ nat" where
"r01_to_r01_r01_snd' r n = r01_binary_expansion' r (2*n + 1)"

lemma r01_to_r01_r01_snd'in01:
  "⋀n. r01_to_r01_r01_snd' r n ∈ {0,1}"
  using real01_binary_expansion'_0or1 by (simp add: r01_to_r01_r01_snd'_def)


definition r01_to_r01_r01_snd_sum :: "real ⇒ nat ⇒ real" where
"r01_to_r01_r01_snd_sum ≡ r01_binary_sum ∘ r01_to_r01_r01_snd'"

definition r01_to_r01_r01_snd :: "real ⇒ real" where
"r01_to_r01_r01_snd = lim ∘ r01_to_r01_r01_snd_sum"

lemma r01_to_r01_r01_snd_def':
  "r01_to_r01_r01_snd r = (∑n. real (r01_binary_expansion' r (2*n + 1)) * (1/2)^(n+1))"
proof -
  have "r01_to_r01_r01_snd_sum r = (λn. ∑i=0..n. real (r01_binary_expansion' r (2*i + 1)) * (1/2)^(i+1))"
    by(auto simp add: r01_to_r01_r01_snd_sum_def r01_binary_sum_def r01_to_r01_r01_snd'_def)
  thus ?thesis
    using lim_sum_ai real01_binary_expansion'_0or1
    by(simp add: r01_to_r01_r01_snd_def)
qed

lemma r01_to_r01_r01_snd_measurable:
 "r01_to_r01_r01_snd ∈ borel_measurable borel"
  unfolding r01_to_r01_r01_snd_def'
  using r01_binary_expansion'_measurable by auto


definition r01_to_r01_r01 :: "real ⇒ real × real" where
"r01_to_r01_r01 r = (r01_to_r01_r01_fst r,r01_to_r01_r01_snd r)"

lemma r01_to_r01_r01_image:
 "r01_to_r01_r01 r ∈ {0..1}×{0..1}"
  using r01_to_r01_r01_fst_def'[of r] r01_to_r01_r01_snd_def'[of r] real01_binary_expansion'_0or1
        binary_expression_gteq0[of "λn. r01_binary_expansion' r (2*n)" 0] binary_expression_leeq1[of "λn. r01_binary_expansion' r (2*n)" 0] binary_expression_gteq0[of "λn. r01_binary_expansion' r (2*n+1)" 0] binary_expression_leeq1[of "λn. r01_binary_expansion' r (2*n+1)" 0]
  by(simp add: r01_to_r01_r01_def)

lemma r01_to_r01_r01_measurable:
 "r01_to_r01_r01 ∈ real_borel →⇩M real_borel ⨂⇩M real_borel"
  unfolding r01_to_r01_r01_def
  using borel_measurable_Pair[of r01_to_r01_r01_fst borel r01_to_r01_r01_snd] r01_to_r01_r01_fst_measurable r01_to_r01_r01_snd_measurable
  by(simp add: borel_prod)

lemma r01_to_r01_r01_3over4:
 "r01_to_r01_r01 (3/4) = (1/2,1/2)"
proof -
  have h0:"r01_binary_expansion' (3/4) 0 = 1"
    by (simp add: r01_binary_expansion'_def)
  have h1:"r01_binary_expansion' (3/4) 1 = 1"
    by (simp add: r01_binary_expansion'_def Let_def of_rat_divide)
  have hn:"⋀n. n>1⟹ r01_binary_expansion' (3/4) n = 0"
  proof -
    fix n :: nat
    assume h:"1 < n"
    show "r01_binary_expansion' (3 / 4) n = 0"
    proof(rule ccontr)
      assume "r01_binary_expansion' (3 / 4) n ≠ 0"
      have "3/4 < (∑i=0..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i))"
      proof -
        have "(∑i=0..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)) = real (r01_binary_expansion' (3/4) 0) * (1/2)^(Suc 0) + (∑i=(Suc 0)..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i))"
          by(rule sum.atLeast_Suc_atMost) (simp add: h)
        also have "... = real (r01_binary_expansion' (3/4) 0) * (1/2)^(Suc 0) + (real (r01_binary_expansion' (3/4) 1) * (1/2)^(Suc 1) + (∑i=(Suc (Suc 0))..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)))"
          using sum.atLeast_Suc_atMost[OF order.strict_implies_order[OF h],of "λi. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)"]
          by simp
        also have "... = 3/4 + (∑i=2..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i))"
          using h0 h1 by(simp add: numeral_2_eq_2)
        also have "... > 3/4"
        proof -
          have "(∑i=2..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)) = (∑i=2..n-1. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)) + real (r01_binary_expansion' (3/4) n) * (1/2)^Suc n"
            by (metis (no_types, lifting) h One_nat_def Suc_pred less_2_cases_iff less_imp_add_positive order_less_irrefl plus_1_eq_Suc sum.cl_ivl_Suc zero_less_Suc)
          hence "real (r01_binary_expansion' (3/4) n) * (1/2)^Suc n ≤ (∑i=2..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i))"
            using ordered_comm_monoid_add_class.sum_nonneg[of "{2..n-1}" "λi. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)"]
            by simp
          moreover have "0 < real (r01_binary_expansion' (3/4) n) * (1/2)^Suc n"
            using ‹r01_binary_expansion' (3 / 4) n ≠ 0› by simp
          ultimately have "0 < (∑i=2..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i))"
            by simp
          thus ?thesis by simp
        qed
        finally show "3 / 4 < (∑i = 0..n. real (r01_binary_expansion' (3 / 4) i) * (1 / 2) ^ Suc i)" .
      qed
      moreover have "(∑i=0..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)) ≤ 3/4"
        using r01_binary_expansion_lr_r_ur[of "3/4" n] r01_binary_expression_eq_lr[of "3/4" n]
        by(simp add: r01_binary_expression_def r01_binary_sum_def)
      ultimately show False by simp
    qed
  qed
  show ?thesis
  proof
    have "fst (r01_to_r01_r01 (3 / 4)) = (∑n. real (r01_binary_expansion' (3 / 4) (2 * n)) * (1 / 2) ^ Suc n)"
      by(simp add: r01_to_r01_r01_def r01_to_r01_r01_fst_def')
    also have "... = 1/2 + (∑n. real (r01_binary_expansion' (3 / 4) (2 * Suc n)) * (1 / 2) ^ Suc (Suc n))"
      using suminf_split_head[of "λn. real (r01_binary_expansion' (3 / 4) (2 * n)) * (1 / 2) ^ Suc n"] binary_expression_summable[of "λn. r01_binary_expansion' (3/4) (2*n)"] real01_binary_expansion'_0or1[of "3/4"] h0
      by simp
    also have "... = 1/2"
    proof -
      have "∀n. real (r01_binary_expansion' (3 / 4) (2 * Suc n)) * (1 / 2) ^ Suc (Suc n) = 0"
        using hn by simp
      hence "(∑n. real (r01_binary_expansion' (3 / 4) (2 * Suc n)) * (1 / 2) ^ Suc (Suc n)) = 0"
        by simp
      thus ?thesis
        by simp
    qed
    finally show "fst (r01_to_r01_r01 (3 / 4)) = fst (1 / 2, 1 / 2)"
      by simp
  next
    have "snd (r01_to_r01_r01 (3 / 4)) = (∑n. real (r01_binary_expansion' (3 / 4) (2 * n + 1)) * (1 / 2) ^ Suc n)"
      by(simp add: r01_to_r01_r01_def r01_to_r01_r01_snd_def')
    also have "... = 1/2 + (∑n. real (r01_binary_expansion' (3 / 4) (2 * Suc n + 1)) * (1 / 2) ^ Suc (Suc n))"
      using suminf_split_head[of "λn. real (r01_binary_expansion' (3 / 4) (2 * n + 1)) * (1 / 2) ^ Suc n"] binary_expression_summable[of "λn. r01_binary_expansion' (3/4) (2*n + 1)"] real01_binary_expansion'_0or1[of "3/4"] h1
      by simp
    also have "... = 1/2"
    proof -
      have "∀n. real (r01_binary_expansion' (3 / 4) (2 * Suc n + 1)) * (1 / 2) ^ Suc (Suc n) = 0"
        using hn by simp
      hence "(∑n. real (r01_binary_expansion' (3 / 4) (2 * Suc n + 1)) * (1 / 2) ^ Suc (Suc n)) = 0"
        by simp
      thus ?thesis
        by simp
    qed
    finally show "snd (r01_to_r01_r01 (3 / 4)) = snd (1 / 2, 1 / 2)"
      by simp
  qed
qed


(* (0,1)×(0,1) ⇒ (0,1). *)
definition r01_r01_to_r01' :: "real × real ⇒ nat ⇒ nat" where
"r01_r01_to_r01' rs ≡ (λn. if even n then r01_binary_expansion' (fst rs) (n div 2)
                                      else r01_binary_expansion' (snd rs) ((n-1) div 2))"

lemma r01_r01_to_r01'in01:
  "⋀n. r01_r01_to_r01' rs n ∈ {0,1}"
  using real01_binary_expansion'_0or1 by (simp add: r01_r01_to_r01'_def)

lemma r01_r01_to_r01'_well_formed:
  assumes "0 < r1" "r1 < 1"
      and "0 < r2" "r2 < 1"
    shows "biexp01_well_formed (r01_r01_to_r01' (r1,r2))"
  using biexp01_well_formed_comb[of "r01_binary_expansion' (fst (r1,r2))" "r01_binary_expansion' (snd (r1,r2))"] r01_binary_expansion_well_formed[of r1] r01_binary_expansion_well_formed[of r2] assms
  by (auto simp add: r01_r01_to_r01'_def)

definition r01_r01_to_r01_sum :: "real × real ⇒ nat ⇒ real" where
"r01_r01_to_r01_sum ≡ r01_binary_sum ∘ r01_r01_to_r01'"

definition r01_r01_to_r01 :: "real × real ⇒ real" where
"r01_r01_to_r01 ≡ lim ∘ r01_r01_to_r01_sum"

lemma r01_r01_to_r01_def':
 "r01_r01_to_r01 (r1,r2) = (∑n. real (r01_r01_to_r01' (r1,r2) n) * (1/2)^(n+1))"
proof -
  have "r01_r01_to_r01_sum (r1,r2) = (λn. (∑i = 0..n. real (r01_r01_to_r01' (r1,r2) i) * (1 / 2) ^ Suc i))"
    by(auto simp add: r01_r01_to_r01_sum_def r01_binary_sum_def)
  thus ?thesis
    using lim_sum_ai[of "λn. r01_r01_to_r01' (r1,r2) n"] r01_r01_to_r01'in01
    by(simp add: r01_r01_to_r01_def)
qed

lemma r01_r01_to_r01_measurable:
 "r01_r01_to_r01 ∈ real_borel ⨂⇩M real_borel →⇩M real_borel"
proof -
  have "r01_r01_to_r01 = (λx. ∑n. real (r01_r01_to_r01' x n) * (1/2)^(n+1))"
    using r01_r01_to_r01_def' by auto
  also have "... ∈ real_borel ⨂⇩M real_borel →⇩M real_borel"
  proof(rule borel_measurable_suminf)
    fix n :: nat
    have "(λx. real (r01_r01_to_r01' x n) * (1 / 2) ^ (n + 1)) = (λr. r * (1/2)^(n+1)) ∘ (λx. real (r01_r01_to_r01' x n))"
      by auto
    also have "... ∈ borel_measurable (borel ⨂⇩M borel)"
    proof(rule measurable_comp[of _ _ borel])
      have "(λx. real (r01_r01_to_r01' x n))
           = (λx. if even n then real (r01_binary_expansion' (fst x) (n div 2)) else real (r01_binary_expansion' (snd x) ((n - 1) div 2)))"
        by (auto simp add: r01_r01_to_r01'_def)
      also have "... ∈  borel_measurable (borel ⨂⇩M borel)"
        using r01_binary_expansion'_measurable by simp
      finally show "(λx. real (r01_r01_to_r01' x n)) ∈ borel_measurable (borel ⨂⇩M borel)" .
    next
      show "(λr::real. r * (1 / 2) ^ (n + 1)) ∈ borel_measurable borel"
        by simp
    qed
    finally show "(λx. real (r01_r01_to_r01' x n) * (1 / 2) ^ (n + 1)) ∈ borel_measurable (borel ⨂⇩M borel)" .
  qed
  finally show ?thesis .
qed

lemma r01_r01_to_r01_image:
  assumes "0 < r1" "r1 < 1"
    shows "r01_r01_to_r01 (r1,r2) ∈ {0<..<1}"
proof -
  obtain i where "r01_binary_expansion' r1 i = 1"
    using r01_binary_expression_ex1[of r1] assms(1,2)
    by auto
  hence hi:"r01_r01_to_r01' (r1,r2) (2*i) = 1"
    by(simp add: r01_r01_to_r01'_def)
  obtain j where "r01_binary_expansion' r1 j = 0"
    using r01_binary_expression_ex0[of r1] assms(1,2)
    by auto
  hence hj:"r01_r01_to_r01' (r1,r2) (2*j) = 0"
    by(simp add: r01_r01_to_r01'_def)
  show ?thesis
    using ai_exists1_gt0[of "r01_r01_to_r01' (r1,r2)"] ai_exists0_less_than1[of "r01_r01_to_r01' (r1,r2)"] r01_r01_to_r01'in01[of "(r1,r2)"] r01_r01_to_r01_def'[of r1 r2] hi hj
    by auto
qed

lemma r01_r01_to_r01_image':
  assumes "0 < r2" "r2 < 1"
    shows "r01_r01_to_r01 (r1,r2) ∈ {0<..<1}"
proof -
  obtain i where "r01_binary_expansion' r2 i = 1"
    using r01_binary_expression_ex1[of r2] assms(1,2)
    by auto
  hence hi:"r01_r01_to_r01' (r1,r2) (2*i + 1) = 1"
    by(simp add: r01_r01_to_r01'_def)
  obtain j where "r01_binary_expansion' r2 j = 0"
    using r01_binary_expression_ex0[of r2] assms(1,2)
    by auto
  hence hj:"r01_r01_to_r01' (r1,r2) (2*j + 1) = 0"
    by(simp add: r01_r01_to_r01'_def)
  show ?thesis
    using ai_exists1_gt0[of "r01_r01_to_r01' (r1,r2)"] ai_exists0_less_than1[of "r01_r01_to_r01' (r1,r2)"] r01_r01_to_r01'in01[of "(r1,r2)"] r01_r01_to_r01_def'[of r1 r2] hi hj
    by auto
qed


lemma r01_r01_to_r01_binary_nth:
  assumes "0 < r1" "r1 < 1"
      and "0 < r2" "r2 < 1"
    shows "r01_binary_expansion' r1 n = r01_binary_expansion' (r01_r01_to_r01 (r1,r2)) (2*n) ∧
           r01_binary_expansion' r2 n = r01_binary_expansion' (r01_r01_to_r01 (r1,r2)) (2*n + 1)"
proof -
  have "⋀n. r01_binary_expansion' (r01_r01_to_r01 (r1,r2)) n = r01_r01_to_r01' (r1,r2) n"
    using r01_r01_to_r01_def'[of r1 r2] biexp01_well_formed_an[of "r01_r01_to_r01' (r1,r2)"] r01_r01_to_r01'_well_formed[of r1 r2] assms
    by simp
  thus ?thesis
    by(simp add: r01_r01_to_r01'_def)
qed

lemma r01_r01__r01__r01_r01_id:
  assumes "0 < r1" "r1 < 1"
          "0 < r2" "r2 < 1"
    shows "(r01_to_r01_r01 ∘ r01_r01_to_r01) (r1,r2) = (r1,r2)"
proof
  show "fst ((r01_to_r01_r01 ∘ r01_r01_to_r01) (r1, r2)) = fst (r1, r2)"
  proof -
    have "fst ((r01_to_r01_r01 ∘ r01_r01_to_r01) (r1, r2)) = r01_to_r01_r01_fst (r01_r01_to_r01 (r1,r2))"
      by(simp add: r01_to_r01_r01_def)
    also have "... = (∑n. real (r01_binary_expansion' (r01_r01_to_r01 (r1, r2)) (2 * n)) * (1 / 2) ^ (n + 1))"
      using r01_to_r01_r01_fst_def'[of "r01_r01_to_r01 (r1,r2)"] by simp
    also have "... = (∑n. real (r01_binary_expansion' r1 n) * (1 / 2) ^ (n + 1))"
      using r01_r01_to_r01_binary_nth[of r1 r2] assms by simp
    also have "... = r1"
      using r01_binary_expression_correct[of r1] assms(1,2)
      by simp
    finally show ?thesis by simp
  qed
next
  show "snd ((r01_to_r01_r01 ∘ r01_r01_to_r01) (r1, r2)) = snd (r1, r2)"
  proof -
    have "snd ((r01_to_r01_r01 ∘ r01_r01_to_r01) (r1, r2)) = r01_to_r01_r01_snd (r01_r01_to_r01 (r1,r2))"
      by(simp add: r01_to_r01_r01_def)
    also have "... = (∑n. real (r01_binary_expansion' (r01_r01_to_r01 (r1, r2)) (2 * n + 1)) * (1 / 2) ^ (n + 1))"
      using r01_to_r01_r01_snd_def'[of "r01_r01_to_r01 (r1,r2)"] by simp
    also have "... = (∑n. real (r01_binary_expansion' r2 n) * (1 / 2) ^ (n + 1))"
      using r01_r01_to_r01_binary_nth[of r1 r2] assms by simp
    also have "... = r2"
      using r01_binary_expression_correct[of r2] assms(3,4)
      by simp
    finally show ?thesis by simp
  qed
qed

text ‹ We first show that ‹M ⨂⇩M N› is a standard Borel space for standard Borel spaces ‹M› and ‹N›.›
lemma pair_measurable[measurable]:
  assumes "f ∈ X →⇩M Y"
      and "g ∈ X' →⇩M Y'"
    shows "map_prod f g ∈ X ⨂⇩M X' →⇩M Y ⨂⇩M Y'"
  using assms by(auto simp add: measurable_pair_iff)

lemma pair_standard_borel_standard:
  assumes "standard_borel M"
      and "standard_borel N"
    shows "standard_borel (M ⨂⇩M N)"
proof -
  ― ‹ First, define the measurable function $\mathbb{R} \times \mathbb{R} \rightarrow \mathbb{R}$.›
  define rr_to_r :: "real × real ⇒ real"
    where "rr_to_r ≡ real_to_01open_inverse ∘ r01_r01_to_r01 ∘ (λ(x,y). (real_to_01open x, real_to_01open y))"
  ― ‹ $\mathbb{R}\times\mathbb{R} \rightarrow (0,1)\times(0,1) \rightarrow (0,1) \rightarrow \mathbb{R}$.›
  have 1[measurable]: "rr_to_r ∈ real_borel ⨂⇩M real_borel →⇩M real_borel"
  proof -
    have "(λ(x,y). (real_to_01open x, real_to_01open y)) ∈ real_borel ⨂⇩M real_borel →⇩M real_borel ⨂⇩M real_borel"
      using borel_measurable_continuous_onI[OF real_to_01open_continuous]
      by simp
    from measurable_restrict_space2[OF _ this,of "{0<..<1}×{0<..<1}"]
    have [measurable]:"(λ(x,y). (real_to_01open x, real_to_01open y)) ∈ real_borel ⨂⇩M real_borel →⇩M restrict_space (real_borel ⨂⇩M real_borel) ({0<..<1}×{0<..<1})"
      by(simp add: split_beta' real_to_01open_01)
    have [measurable]: "r01_r01_to_r01 ∈ restrict_space (real_borel ⨂⇩M real_borel) ({0<..<1}×{0<..<1}) →⇩M restrict_space real_borel {0<..<1}"
      using r01_r01_to_r01_image' by(auto intro!: measurable_restrict_space3[OF r01_r01_to_r01_measurable])
    thus ?thesis
      using borel_measurable_continuous_on_restrict[OF real_to_01open_inverse_continuous]
      by(simp add: rr_to_r_def)
  qed
  ― ‹ Next, define the measurable function $\mathbb{R}\rightarrow \mathbb{R}\times\mathbb{R}$.›
  define r_to_01 :: "real ⇒ real"
    where "r_to_01 ≡ (λr. if r ∈ real_to_01open -` (r01_to_r01_r01 -` ({0<..<1}×{0<..<1})) then real_to_01open r else 3/4)"
  define r01_to_r01_r01' :: "real ⇒ real × real"
    where "r01_to_r01_r01' ≡ (λr. if r ∈ r01_to_r01_r01 -` ({0<..<1}×{0<..<1}) then r01_to_r01_r01 r else (1/2,1/2))"
  define r_to_rr :: "real ⇒ real × real"
    where "r_to_rr ≡ (λ(x,y). (real_to_01open_inverse x, real_to_01open_inverse y)) ∘ r01_to_r01_r01' ∘ r_to_01"
  ― ‹ $\mathbb{R} \rightarrow (0,1) \rightarrow (0,1)\times(0,1) \rightarrow \mathbb{R}\times\mathbb{R}$.›
  have 2[measurable]: "r_to_rr ∈ real_borel →⇩M real_borel ⨂⇩M real_borel"
  proof -
    have 1: "{0<..<1}×{0<..<1} ∈ sets (restrict_space (real_borel ⨂⇩M real_borel) ({0..1}×{0..1}))"
      by(auto simp: sets_restrict_space_iff)
    have 2[measurable]: "real_to_01open ∈ real_borel →⇩M restrict_space real_borel {0<..<1}"
      using measurable_restrict_space2[OF _ borel_measurable_continuous_onI[OF real_to_01open_continuous] ,of "{0<..<1}"]
      by(simp add: real_to_01open_01)
    have 3: "real_to_01open -` space (restrict_space real_borel {0<..<1}) = UNIV"
      using real_to_01open_01 by auto
    have "r01_to_r01_r01 ∈ restrict_space real_borel {0<..<1} →⇩M restrict_space (real_borel ⨂⇩M real_borel) ({0..1}×{0..1})"
      using r01_to_r01_r01_image measurable_restrict_space3[OF r01_to_r01_r01_measurable] by simp
    note 4 = measurable_sets[OF this 1]
    note 5 = measurable_sets[OF 2 4,simplified vimage_Int 3,simplified]
    have [measurable]:"r_to_01 ∈ real_borel →⇩M restrict_space real_borel {0<..<1}"
      unfolding r_to_01_def
      by(rule  measurable_If_set) (auto intro!: measurable_restrict_space2 simp: 5)
    have [measurable]: "r01_to_r01_r01' ∈ restrict_space real_borel {0<..<1} →⇩M restrict_space (real_borel ⨂⇩M real_borel) ({0<..<1}×{0<..<1})"
      using 4 r01_to_r01_r01_measurable
      by(auto intro!: measurable_restrict_space3 simp: r01_to_r01_r01'_def)
    have [measurable]: "(λ(x,y). (real_to_01open_inverse x, real_to_01open_inverse y)) ∈ restrict_space (real_borel ⨂⇩M real_borel) ({0<..<1}×{0<..<1}) →⇩M real_borel ⨂⇩M real_borel"
      using borel_measurable_continuous_on_restrict[OF continuous_on_Pair[OF continuous_on_compose[of "{0<..<1::real}×{0<..<1::real}",OF continuous_on_fst[OF continuous_on_id'],simplified,OF real_to_01open_inverse_continuous] continuous_on_compose[of "{0<..<1::real}×{0<..<1::real}",OF continuous_on_snd[OF continuous_on_id'],simplified,OF real_to_01open_inverse_continuous]]]
      by(simp add: split_beta' borel_prod)
    show ?thesis
      by(simp add: r_to_rr_def)
  qed
  have 3: "⋀x. r_to_rr (rr_to_r x) = x"
    using r01_to_r01_r01_image r01_r01_to_r01_image r01_r01__r01__r01_r01_id real_to_01open_01  real_to_01open_inverse_correct' fun_cong[OF real_to_01open_inverse_correct]
    by(auto simp add: r01_to_r01_r01'_def r_to_01_def comp_def split_beta' r_to_rr_def rr_to_r_def)

  interpret s1: standard_borel M by fact
  interpret s2: standard_borel N by fact
  show ?thesis
    by(auto intro!: standard_borelI[where f="rr_to_r ∘ map_prod s1.f s2.f" and g="map_prod s1.g s2.g ∘ r_to_rr"] simp: 3 space_pair_measure)
qed

lemma pair_standard_borel_spaceUNIV:
  assumes "standard_borel_space_UNIV M"
      and "standard_borel_space_UNIV N"
    shows "standard_borel_space_UNIV (M ⨂⇩M N)"
  apply(rule standard_borel_space_UNIVI')
  using assms pair_standard_borel_standard[of M N]
  by(auto simp add: standard_borel_space_UNIV_def standard_borel_space_UNIV_axioms_def space_pair_measure)


locale pair_standard_borel = s1: standard_borel M + s2: standard_borel N
  for M :: "'a measure" and N :: "'b measure"
begin

sublocale standard_borel "M ⨂⇩M N"
  by(auto intro!: pair_standard_borel_standard)

end

locale pair_standard_borel_space_UNIV = s1: standard_borel_space_UNIV M + s2: standard_borel_space_UNIV N
  for M :: "'a measure" and N :: "'b measure"
begin

sublocale pair_standard_borel M N
  by standard

sublocale standard_borel_space_UNIV "M ⨂⇩M N"
  by(auto intro!: pair_standard_borel_spaceUNIV
      simp: s1.standard_borel_space_UNIV_axioms s2.standard_borel_space_UNIV_axioms)

end


text ‹$\mathbb{R}\times\mathbb{R}$ is a standard Borel space.›
interpretation real_real : pair_standard_borel_space_UNIV real_borel real_borel
  by(auto intro!: pair_standard_borel_spaceUNIV simp: real.standard_borel_space_UNIV_axioms pair_standard_borel_space_UNIV_def)

subsection ‹ $\mathbb{N}\times\mathbb{R}$ ›
text ‹ $\mathbb{N}\times\mathbb{R}$ is a standard Borel space. ›
interpretation nat_real: pair_standard_borel_space_UNIV nat_borel real_borel
  by(auto intro!: pair_standard_borel_spaceUNIV
       simp: real.standard_borel_space_UNIV_axioms nat.standard_borel_space_UNIV_axioms pair_standard_borel_space_UNIV_def)

end